The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

minus(x, y) → if(gt(x, y), x, y)
if(true, x, y) → s(minus(p(x), y))
if(false, x, y) → 0
p(0) → 0
p(s(x)) → x
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
div(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → 0
if2(true, x, y) → s(div(minus(x, y), y))
if2(false, x, y) → 0

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
minus(s(x13_3), 0) →⁺ s(minus(x13_3, 0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [x13_3 / s(x13_3)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)